\begin{tabbing}
$\forall$$w$:World.
\\[0ex]FairFifo
\\[0ex]$\Rightarrow$ \=($\forall$$e$:E.\+
\\[0ex]state\_after($e$) = ($\lambda$$x$,$q$. s(loc($e$);time($e$)+1).$x$($q$ {-} 1)) $\in$ $x$:Id$\rightarrow\mathbb{Q}\rightarrow$vartype(loc($e$);$x$))
\-
\end{tabbing}